(set-logic QF_BV)
(declare-fun _substvar_39_ () (_ BitVec 1))
(declare-fun _substvar_38_ () (_ BitVec 32))
(declare-fun _substvar_48_ () (_ BitVec 1))
(declare-fun _substvar_51_ () (_ BitVec 1))
(declare-fun _substvar_31_ () (_ BitVec 1))
(assert (= true (bvult (_ bv0 32) _substvar_38_)))
(assert (= _substvar_51_ (_ bv0 1)))
(assert (= (= _substvar_48_ (_ bv1 1)) (bvule ((_ extract 31 0) (_ bv2 64)) _substvar_38_)))
(assert (= _substvar_31_ _substvar_48_))
(assert (= (_ bv0 1) (bvand _substvar_39_ _substvar_31_)))
(assert (= false (bvule _substvar_38_ ((_ extract 31 0) (_ bv4 64)))))
(check-sat)
(exit)
